Section: New Results

Unconditional Soundness (Objective 2)

Participant : Hubert Comon-Lundh.

Hubert Comon-Lundh, Véronique Cortier and Guillaume Scerri [31] show how one can drop one of the assumptions of computational soundness results. However, the proofs remain very complicated and there are still assumptions such as the absence of key cycles, or no dynamic corruption... that are still necessary for all these results.

Gergei Bana and Hubert Comon-Lundh investigated a completely different approach to formal security proofs [25] , which does not make any such assumptions. The idea can be stated in a nutshell: whereas all existing formal models state the attacker's abilities, they propose to formally state what the attacker cannot do.

This makes a big difference, since the soundness need only to be proved formula by formula and only the very necessary assumptions are used for such formulas (for instance, no absence of key cycles is needed). This does not need to be proved again when a primitive is added.

The counterpart of this nice approach is the difficulty of the automation: a tool is required for checking the consistency of a set of axioms, together with the conditions accumulated along a trace. This problem is the subject of research for the next year(s).